Previous | 
Home
Section: Partnerships and Cooperations
National Initiatives
ANR
AbstractCell
-
Title: Formal abstraction of quantitative semantics for protein-protein interaction cellular network models
-
See also: http://www.di.ens.fr/ feret/abstractcell
-
Abstract: The overall goal of this project is to investigate formal foundations and computational aspects of both the stochastic and differential approximate semantics for rule-based models. We want to relate these semantics formally, then we want to design sound approximations for each of these semantics (by abstract interpretation) and investigate scalable algorithms to compute the properties of both the stochastic and the differential semantics. Jérôme Feret is the principal investigator for this project.
AstréeA
-
Title: Static Analysis of Embedded Asynchronous Real-Time Software
-
See also: http://www.astreea.ens.fr
-
Abstract: The focus of the AstréeA project is on the development of static analysis by abstract interpretation to check the safety of large-scale asynchronous embedded software. During the Thésée ANR project (2006–2010), we developed a concrete and abstract models of the ARINC 653 operating system and its scheduler, and a first analyzer prototype. The gist of the AstréeA project is the continuation of this effort, following the recipe that made the success of Astrée : an incremental refinement of the analyzer until reaching the zero false alarm goal. The refinement concerns: the abstraction of process interactions (relational and history-sensitive abstractions), the scheduler model (supporting more synchronisation primitives and taking priorities into account), the memory model (supporting volatile variables), and the abstraction of dynamical data-structures (linked lists). Patrick Cousot is the principal investigator for this project.
Verasco
-
Others partners: Airbus France (France), IRISA (France), Inria Saclay (France)
-
See also: http://www.systematic-paris-region.org/fr/projets/verasco
-
Abstract: The usefulness of verification tools in the development and certification of critical software is limited by the amount of trust one can have in their results. A first potential issue is unsoundness of a verification tool: if a verification tool fails (by mistake or by design) to account for all possible executions of the program under verification, it can conclude that the program is correct while it actually misbehaves when executed. A second, more insidious, issue is miscompilation: verification tools generally operate at the level of source code or executable model; a bug in the compilers and code generators that produce the executable code that actually runs can lead to a wrong executable being generated from a correct program.
The project Verasco advocates a mathematically-grounded solution to the issues of formal verifying compilers and verification tools. We set out to develop a generic static analyzer based on abstract interpretation for the C language, along with a number of advanced abstract domains and domain combination operators, and prove the soundness of this analyzer using the Coq proof assistant. Likewise, we will continue our work on the CompCert C formally-verified compiler, the first realistic C compiler that has been mechanically proved to be free of any miscompilation will be continued. Finally, the tool qualification issues that must be addressed before formally-verified tools can be used in the aircraft industry, will be investigated.